$\forall$$a$:$\mathbb{Z}$, $b$:$\mathbb{N}^{+}$. $\exists$$q$:$\mathbb{Z}$. $\exists$$r$:int\_seg(0; $b$). ($a$ = (($q$ $\ast$ $b$) + $r$))